Nuprl Lemma : R-sub-plus-left
11,40
postcript
pdf
A
,
B
:es_realizer{i:l}. R-sub{i:l}(
A
; Rplus(
A
;
B
))
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
P
Q
,
P
Q
Lemmas
es
realizer
wf
,
R-sub-lemma1
origin
A,B:es_realizer{i:l}. R-sub{i:l}(A; Rplus(A; B)) A,B:es_realizer{i:l}. R-sub{i:l}(A; Rplus(A; B)) 
Tx:A. B(x)
Q
Q